/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.bool;


/** Base class for {@link GBF_And} and {@link GBF_Or} nodes. */
abstract class GBF_AndOrBase extends BooleanFormula {
    BooleanFormula[] subexprs;


    protected GBF_AndOrBase() { subexprs = null; }
    
    protected GBF_AndOrBase(BooleanFormula[] subexprs) {
	this.subexprs = subexprs;
    }

    protected GBF_AndOrBase(BooleanFormula e1, boolean absorb1, BooleanFormula e2, boolean absorb2) {
	absorb1 = absorb2 = false;
	BooleanFormula[] sub1 = absorb1 ? ((GBF_AndOrBase)e1).subexprs : null;
	BooleanFormula[] sub2 = absorb2 ? ((GBF_AndOrBase)e2).subexprs : null;
	int nsubex = (absorb1 ? sub1.length : 1) + (absorb2 ? sub2.length : 1);
	subexprs = new BooleanFormula[nsubex];
	int ni = 0;
	if (absorb1)
	    for (int j=0; j<sub1.length; j++)
		subexprs[ni++] = sub1[j];
	else
	    subexprs[ni++] = e1;
	
	if (absorb2)
	    for (int j=0; j<sub2.length; j++)
		subexprs[ni++] = sub2[j];
	else
	    subexprs[ni++] = e2;
    }

    void setSubexprs(BooleanFormula[] subexprs) {
	this.subexprs = subexprs;
    }


    protected boolean checkConstantValued() {
	for (int i=0; i<subexprs.length; i++)
	    if (!subexprs[i].isConstantValued()) 
		return false;
	return true;
    }
    

    /** returns the # of boolean vars used by this expression */
    int getNumVars() {
	int maxVar = 0;
	for (int i=0; i<subexprs.length; i++) {
	    int mhere = subexprs[i].getNumVars();
	    if (mhere > maxVar)
		maxVar = mhere;
	}
	return maxVar;
    }

    /** Returns a new copy of the same node type: And or Or */
    abstract GBF_AndOrBase allocCopy();

    // two routines to help define visitors' behavior on AND/OR nodes
    
    /**
     * Auxiliary routine: recursively apply visitor to the children
     * of a given And/Or node
     *
     * @param visitor visitor whose forXXXX methods return BooleanFormulas
     * @return array of this and/or node's children transformed by the visitor
     */
    BooleanFormula[] getVisitedChildren(GBF_V visitor) {
	int nsubexprs = subexprs.length;
	BooleanFormula[] newSubexprs = new BooleanFormula[nsubexprs];
	for (int i=0; i<nsubexprs; i++)
	    newSubexprs[i] = (BooleanFormula)(subexprs[i].acceptVisitor(visitor));
	return newSubexprs;
    }

    /**
       Apply the given visitor to this and/or node's children; if it
       doesn't touch them, return this node; else, copy this node
       and replace children with children transformed by the visitor

       @param visitor visitor whose forXXXX methods return BooleanFormulas
       @return this if visitor doesn't touch children, else same-type node with transformed children
     */
    GBF_AndOrBase transformChildrenByVisitor(GBF_V visitor) {
	BooleanFormula[] newSubexprs = getVisitedChildren(visitor);
	// check whether any of the subexprs have changed
	// if all are the same as before, we can reuse the existing node
	boolean needNewNode = false;
	for (int i=0; i<newSubexprs.length && !needNewNode; i++)
	    needNewNode |= (newSubexprs[i] != subexprs[i]);

	if (!needNewNode)
	    return this;
	else {
	    GBF_AndOrBase newNode =
		allocCopy();  // create an AND node if (this instanceof GBF_And),
	                      // an OR node if (this instanceof GBF_Or)
	    newNode.setSubexprs(newSubexprs);
	    return newNode;
	}
    }

    /** convert list of subexpressions to string */
    protected String subex2string() { //if (true) return "sub";
	String s = "";
	for (int i=0; i<subexprs.length; i++)
	    s = s + subexprs[i].dbg()+" ";
	return s;
    }

    /**
     * Tests whether another AND/OR node is of the same type as this,
     * and has equal children in the same order.
     */
    public boolean equals(Object obj_) {
	if (!obj_.getClass().equals(this.getClass())) return false;
	GBF_AndOrBase that = (GBF_AndOrBase)obj_;
	if (subexprs.length != that.subexprs.length) return false;
	for (int i=0; i<subexprs.length; i++)
	    if (!subexprs[i].equals(that.subexprs[i]))
		return false;
	return true;
    }
}
